We introduce a controlled concurrency framework, derived from the Owicki-Gries method, for describing\na hardware interface in detail sufficient to support the modelling and verification of small,\nembedded operating systems (OS�s) whose run-time responsiveness is paramount. Such real-time\nsystems run with interrupts mostly enabled, including during scheduling. That differs from many\nother successfully modelled and verified OS�s that typically reduce the complexity of concurrency by\nrunning on uniprocessor platforms and by switching interrupts off as much as possible.\nOur framework builds on the traditional Owicki-Gries method, for its fine-grained concurrency\nis needed for high-performance system code. We adapt it to support explicit concurrency control,\nby providing a simple, faithful representation of the hardware interface that allows software to control\nthe degree of interleaving between user code, OS code, interrupt handlers and a scheduler that\ncontrols context switching. We then apply this framework to model the interleaving behavior of the\ne Chronos OS, a preemptible real-time OS for embedded micro-controllers. We discuss the accuracy\nand usability of our approach when instantiated to model the eChronos OS. Both our framework and\nthe e Chronos model are formalised in the Isabelle/HOL theorem prover, taking advantage of the high\nlevel of automation in modern reasoning tools.
Loading....